Nuprl Lemma : qeq_wf
11,40
postcript
pdf
r
,
s
:b-union(
; (
:
int_nzero)). qeq(
r
;
s
)
latex
Definitions
(
i
=
j
)
,
ff
,
tt
,
if
b
then
t
else
f
fi
,
qeq(
r
;
s
)
,
t
T
,
x
:
A
.
B
(
x
)
,
,
int_nzero
,
b-union(
A
;
B
)
Lemmas
int
nzero
wf
,
b-union
wf
,
btrue
wf
,
eq
int
wf
origin
r,s:b-union(
; (: 
int_nzero)). qeq(r; s) 
r,s:b-union(; (: int_nzero)). qeq(r; s) 
j) Tx:A. B(x)